Nuprl Lemma : xxtrans_functionality_wrt_breqv 13,42

T:Type, RR':(TT). (R <>{TR' (trans(T;R trans(T;R')) 
latex


Upgen algebra 1
Definitions of StatementE <>{TE', trans(T;E)
DefinitionsP & Q, x,yt(x;y), t  T, P  Q, trans(T;E), P  Q, E <>{TE', P  Q, , x:AB(x), x(s1,s2)
Lemmasiff wf, trans functionality wrt iff, trans wf, iff functionality wrt iff

origin